@ @p
contradiction:=for_all(bool,(b:bool)b):bool. {all |bool| can be proved}
by_contradiction(b:bool;p:proof(contradiction)):=
 specialize(bool,(b:bool)b,b,p):proof(b). {this proves |b| if $\T\;$|contradiction|}
@#
not(b:bool):=for_all(proof(b),(p:proof(b))contradiction):bool.
	{$\lnot\;b$,
		constructive negation: all proofs of |b| lead to a contradiction}
impossible(b:bool;p:proof(b);q:proof(not(b))):=
 specialize(proof(b),(p:proof(b))contradiction,p,q):proof(contradiction).
	{$\T\;b$ and $\T\;\lnot b$ is contradictory}
hence_not(b:bool;p:(q:proof(b))proof(contradiction)):=
 generalize(proof(b),(q:proof(b))contradiction,p):proof(not(b)).
	{if $\T\;b$ leads to a contradiction, then $\T\;\lnot b$}
@#
modus_tollens(a,b:bool;p:proof(implies(a,b));q:proof(not(b))):=
 hence_not(a,(r:proof(a))impossible(b,modus_ponens(a,b,p,r),q)):proof(not(a)).
	{if $a$ implies $b$ and $\lnot b$ then $\lnot a$}
@#
double_not(b:bool;p:proof(b)):=
 hence_not(not(b),(q:proof(not(b)))impossible(b,p,q)):proof(not(not(b))).
	{if $b$ then $\lnot\lnot b$}
@#
negation(t:atom;p:(x:t)bool):=(x:t)not(p(x)):(x:t)bool.
	{for all $x$ we have $\lnot p(x)$}
weakly_exists(t:atom;p:(x:t)bool):=not(for_all(t,negation(t,p))):bool.
	{$\lnot\forall x\;\lnot p(x)$}
@#
step1(t:atom;p:(x:t)bool;q:proof(exists(t,p));r:proof(for_all(t,negation(t,p)))):=
 specialize(t,negation(t,p),choose(t,p,q),r):proof(not(p(choose(t,p,q)))).
	{if $\exists x\;p(x)$ and $\forall x\;\lnot p(x)$ then
		we have an $x$ with both $p(x)$ and $\lnot p(x)$}
step2(t:atom;p:(x:t)bool;q:proof(exists(t,p));r:proof(for_all(t,negation(t,p)))):=
 impossible(p(choose(t,p,q)),thus(t,p,q),step1(t,p,q,r)):proof(contradiction).
	{and that's a contradiction}
step3(t:atom;p:(x:t)bool;q:proof(exists(t,p))):=
 hence_not(for_all(t,negation(t,p)),step2(t,p,q)):proof(weakly_exists(t,p)).
	{hence $\lnot\forall x\;\lnot p(x)$}
fact1(t:atom;p:(x:t)bool):=
 implication(exists(t,p),weakly_exists(t,p),step3(t,p)):
 proof(implies(exists(t,p),weakly_exists(t,p))).
	{we have proved constructively that $\exist$ implies $\lnot\forall\lnot$}
@#
nonconstructive(t:atom;p:(x:t)bool):=#:
 proof(implies(weakly_exists(t,p),exists(t,p))).
	{nonconstructivists assume that the converse is also true}

@ @p

trivial(b:bool):=proof(implies(b,b)):atom.
	{$\T b\Rightarrow b$}
prop1(b:bool):=(p:trivial(b))b:(p:trivial(b))bool.
	{a mapping that takes a tautology into a specific |bool|}
prop2(b:bool):=(p:trivial(b))not(b):(p:trivial(b))bool.
	{similarly for its negation}
trick(b:bool):=for_all(trivial(b),prop2(b)):bool.
	{for all proofs of |trivial(b)| there's a proof of $\lnot b$}
step1(b:bool;q:proof(trick(b))):=
 specialize(trivial(b),prop2(b),imp_refl(b),q):proof(not(b)).
	{if so, there's a proof of $\lnot b$}
step2(b:bool;p:proof(not(not(b)));q:proof(trick(b))):=
 impossible(not(b),step1(b,q),p):proof(contradiction).
	{we can't prove both $\lnot\lnot b$ and |trick(b)|}
step3(b:bool;p:proof(not(not(b)))):=
 hence_not(trick(b),step2(b,p)):proof(weakly_exists(trivial(b),prop1(b))).
	{hence $\lnot\lnot b$ gives weak existence of $b$}
step4(b:bool;p:proof(not(not(b)))):=
 modus_ponens(weakly_exists(trivial(b),prop1(b)),exists(trivial(b),prop1(b)),
  nonconstructive(trivial(b),prop1(b)),step3(b,p)):
 proof(exists(trivial(b),prop1(b))).
	{and we can apply the nonconstructive axiom to get what we want:}
excluded_middle(b:bool;p:proof(not(not(b)))):=
 thus(trivial(b),prop1(b),step4(b,p)):proof(b).
	{$\T\;\lnot\lnot b$ implies $\T\;b$}